M:MsgA, l:IdLnk, tg:Id. M.din(l,tg)  Type 

latex

Definitions	MsgA, M.din(l,tg), f(x)?z, x. t(x), Knd, KindDeq, rcv(l,tg), x:A. B(x), Top, Id, t  T, IdLnk
Lemmas	IdLnk wf, Id wf, top wf, rcv wf, Kind-deq wf, Knd wf, fpf-cap wf, msga wf